Skip to content

feat: add bitblasting circuit for BitVec.cpop#12433

Merged
hargoniX merged 174 commits intoleanprover:masterfrom
opencompl:popcount-clean-frfr
Mar 2, 2026
Merged

feat: add bitblasting circuit for BitVec.cpop#12433
hargoniX merged 174 commits intoleanprover:masterfrom
opencompl:popcount-clean-frfr

Conversation

@luisacicolini
Copy link
Contributor

@luisacicolini luisacicolini commented Feb 11, 2026 •
edited
Loading

This PR adds a bitblasting circuit for BitVec.cpop with a divide-and-conquer for a parallel-prefix-sum.

This is the most efficient circuit we could fine, after comparing with Kernighan's algorithm and with the intuitive addition circuit.

@luisacicolini
Copy link
Contributor Author

luisacicolini commented Feb 11, 2026

changelog-library

@github-actions github-actions bot added the changelog-library Library label Feb 11, 2026
luisacicolini
luisacicolini commented Feb 11, 2026
View reviewed changes
luisacicolini
luisacicolini commented Feb 11, 2026
View reviewed changes
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 11, 2026
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Feb 11, 2026 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 57c5efe309336d173bee324b28d7fefdd955f9df --onto 4cdc199f772977113bd6c1bf87a6c02b78d5c4d3. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-11 16:16:02)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 92aec450578f47e4a04abcd72ad6c2372ed17b2c --onto 6ca23a7b8bee57152110ce500ce795148707d4ed. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-13 14:51:27)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 043b8a765a98b223d0ecef47f076c28aefb57d28 --onto 91bd6e19a7b7aca769f9720e1127c768df0cd2a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-18 16:30:32)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4fbc5d3c2a85444c662485317d8b1e2899e3d3dd --onto 309f44d00757482e1c5a2b2427fdca818a24615a. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-20 14:59:07)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase dc760cf54af838af03a4668ad94f8cee19262f29 --onto c595413fccaa47ebdc399d9b817c17425687fc26. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-25 16:16:31)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 846420dabab15cec6d4c095069dc34d7a9ba4b59 --onto c595413fccaa47ebdc399d9b817c17425687fc26. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-26 15:26:01)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 846420dabab15cec6d4c095069dc34d7a9ba4b59 --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-27 14:42:15)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Feb 11, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 57c5efe309336d173bee324b28d7fefdd955f9df --onto 03dc334f73259e1bae0b8f2b80a39a82e1de3df6. You can force reference manual CI using the force-manual-ci label. (2026-02-11 16:16:04)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 92aec450578f47e4a04abcd72ad6c2372ed17b2c --onto 03dc334f73259e1bae0b8f2b80a39a82e1de3df6. You can force reference manual CI using the force-manual-ci label. (2026-02-13 14:51:28)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 92aec450578f47e4a04abcd72ad6c2372ed17b2c --onto 9da8f5dce42832b8411d58446653f3640a94a6e3. You can force reference manual CI using the force-manual-ci label. (2026-02-13 15:44:30)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 043b8a765a98b223d0ecef47f076c28aefb57d28 --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-18 16:30:34)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4fbc5d3c2a85444c662485317d8b1e2899e3d3dd --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-20 14:59:09)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase dc760cf54af838af03a4668ad94f8cee19262f29 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-25 16:16:34)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 846420dabab15cec6d4c095069dc34d7a9ba4b59 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-26 15:26:04)

luisacicolini
luisacicolini commented Feb 13, 2026
View reviewed changes
bollu
bollu reviewed Feb 13, 2026
View reviewed changes
Copy link
Contributor

@bollu bollu left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did a full pass. I've checked for nonterminal simps, naming conventions, and I've asked to move all the casts that occur in the theorem statements to become hypotheses with default arguments (it makes the theorem statement much more sane to read).

@luisacicolini luisacicolini requested a review from bollu February 16, 2026 10:51
bollu
bollu reviewed Feb 18, 2026
View reviewed changes
Copy link
Contributor

@bollu bollu left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Overall LGTM. I left some naming / stylistic questions in the APIs developed in Lemmas and Bitblast. I didn't read over the proofs in the AIG too carefully, I but they look right to me structurally: They have lemmas for denoting each component, and they rewrite away the AIG junk, and finally apply the denotation.

hargoniX
hargoniX requested changes Feb 27, 2026
View reviewed changes
Copy link
Contributor

@hargoniX hargoniX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks pretty good now, I think after this round we can merge 👍

hargoniX
hargoniX reviewed Mar 2, 2026
View reviewed changes
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean Outdated
let extendedBits := res.vec
blastCpopTree aig ⟨extendedBits, by omega⟩
else if hw' : 0 < w then
⟨aig, x⟩
Copy link
Contributor

@hargoniX hargoniX Mar 2, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
⟨aig, x⟩
⟨aig, x⟩

@hargoniX hargoniX enabled auto-merge March 2, 2026 13:19
@hargoniX hargoniX added this pull request to the merge queue Mar 2, 2026
Merged via the queue into leanprover:master with commit df74c80 Mar 2, 2026
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hargoniX hargoniX hargoniX requested changes

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

+1 more reviewer

@bollu bollu bollu left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@luisacicolini @leanprover-bot @bollu @hargoniX